VERS5 
NIL 
((DEMORGAN NORMAL#5) (DEMORGAN1 NORMAL#6) (EXCLUDED_MIDDLE NORMAL#7) (TRANS_COND NORMAL#8) (IRREFLEXIVITY_OF_ORDER NATNUM#7) (TRANSITIVITY_OF_ORDER NATNUM#8) (ZEROLEAST1 NATNUM#9) (SUCCESSOR1 NATNUM#11) (SUCCESSOR2 NATNUM#12) (SUCCESSORLESS NATNUM#13) (SUCCESSOREQ NATNUM#14) (ZEROLEAST2 NATNUM#15) (ZEROLEAST3 NATNUM#16) (ZERO_NOT_SUCCESSOR NATNUM#17) (PLUSDEF1 NATNUM#24) (LPLUSCAN NATNUM#26) (RPLUSCAN NATNUM#27) (ADDTOZERO NATNUM#28) (COMMUTADD NATNUM#29) (TIMSUCC NATNUM#33) (LTIMESCAN NATNUM#34) (RTIMESCAN NATNUM#35) (COMMUTMULT NATNUM#36) (LTIMESTOZERO NATNUM#37) (RTIMESTOZERO NATNUM#38) (LDISTRIB NATNUM#39) (RDISTRIB NATNUM#40) (PROOF_BY_INDUCTION INDUCTION#1) (INDUCTIVE_DEFINITION INDUCTION#5) (PROOF_BY_DOUBLEINDUCTION INDUCTION#6) (HIGH_ORDER_NATNUM_DEFINITION INDUCTION#10) (INFINITE_DESCENT INDUCTION#11) (LESSEQDEF LESSEQ#3) (SUCCESSORLESSEQ LESSEQ#4) (SUCCESSORFACTS LESSEQ#4) (TRANS_LESSEQ LESSEQ#5) (LESS_LESSEQ_FACT1 LESSEQ#6) (ZEROLEAST LESSEQ#7) (ONELEASTSUCC LESSEQ#8) (ZERO_NON_LESS_SUCCESSOR LESSEQ#9) (SUCC_LESS_LESS LESSEQ#10) (SUCC_LESSEQ_LESSEQ LESSEQ#11) (LESSEQ_LESSEQ_SUCC LESSEQ#12) (LESS_SUCC_LESSEQ LESSEQ#13) (LESS_LESSEQSUCC LESSEQ#14) (LEQ_LEQ_EQ LESSEQ#15) (TRICHOTOMY LESSEQ#16) (MINUSDEF MINUS#2) (MINUS_SORT MINUS#3) (MINUSFACT3 MINUS#4) (MINUSFACT5 MINUS#5) (SUCCESSOR_MINUS MINUS#6) (MINUSFACT10 MINUS#7) (MINUSFACT11 MINUS#8) (N_LESS_N MINUS#9) (MINUS1 MINUS#10) (TOTAL_SUBTRACTION MINUS#11) (INEQUALITY_LAW MINUS#12) (ADD_LESSEQ MINUS#13) (ADD_ONE MINUS#14) (EPSILONDEF SETS#4) (SET_EXTENSIONALITY SETS#5) (INTERDEF SETS#7) (UNIONDEF SETS#9) (INCLUSIONDEF SETS#11) (DOUBLE_INCLUSION SETFACTS#1) (ALLDEF SUMS#7) (SOMEDEF SUMS#8) (SUMDEF SUMS#9) (UNDEF SUMS#10) (DISJPAIR_DEF SUMS#12) (DISJOINTDEF SUMS#14) (ALLFACT SUMFACTS#1) (SOMEFACT SUMFACTS#2) (UNIONFACT1 SUMFACTS#3) (SUMSORT SUMFACTS#4) (NORMAL NORMAL#1 NORMAL#2 NORMAL#3 NORMAL#4) (SUCCFACTS NATNUM#11 NATNUM#12 NATNUM#13 NATNUM#14 NATNUM#15 NATNUM#16 NATNUM#17) (TIMESFACTS NATNUM#30 NATNUM#32 NATNUM#33 NATNUM#34 NATNUM#35 NATNUM#36 NATNUM#37 NATNUM#38 NATNUM#39 NATNUM#40) (PLUSFACTS NATNUM#21 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 NATNUM#29 NATNUM#39 NATNUM#40) (SIMPINFO NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 SETS#14)) (|∀P Q R.(P∨Q)∧R≡P∧R∨Q∧R| . (AXIOM (TM& . |∀P Q R.(P∨Q)∧R≡P∧R∨Q∧R|)) . ((R . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (Q . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (P . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .))) . NIL . (NORMAL#1) . NIL . NORMAL . NIL . 1 .)(NIL . (DECL LESSP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: <) (BINDINGPOWER: 920)) . ((LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . NATNUM#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 1 .)(NIL . (DECL ADD1 (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (POSTFIXNAME: /') (BINDINGPOWER: 975)) . ((ADD1 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 975) (POSTFIX& . /')) . NATNUM#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 2 .)(NIL . (DECL PLUS (INFIXNAME: +) (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 930)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 3 .)(NIL . (DECL TIMES (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: *) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 935)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . NATNUM#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 4 .)(NIL . (DECL (I J K N M) (SORT: (TM& . NATNUM)) (TYPE: (TY& . GROUND))) . ((M . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (N . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (K . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (J . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (I . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 5 .)(NIL . (DECL (A B C SET) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((SET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (C . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (B . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (A . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 6 .)(NIL . (DECL MINUS (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (INFIXNAME: -) (BINDINGPOWER: 940)) . ((MINUS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 940) (INFIX& . -)) . MINUS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . MINUS . NIL . 1 .)(NIL . (DECL (XV YV ZV) (TYPE: (TY& . GROUND)) (SORT: (TM& . URELEMENT))) . ((ZV . (GROUND . (SYMBOL& URELEMENT NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (YV . (GROUND . (SYMBOL& URELEMENT NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (XV . (GROUND . (SYMBOL& URELEMENT NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (URELEMENT . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 1 .)(NIL . (DECL (AV BV) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((BV . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .)) (AV . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 2 .)(|∀P Q R.R∧(P∨Q)≡R∧P∨R∧Q| . (AXIOM (TM& . |∀P Q R.R∧(P∨Q)≡R∧P∨R∧Q|)) . (R Q P) . NIL . (NORMAL#2) . NIL . NORMAL . NIL . 2 .)(|∀P Q R.R∧(P∨Q)≡P∧R∨Q∧R| . (AXIOM (TM& . |∀P Q R.R∧(P∨Q)≡P∧R∨Q∧R|)) . (R Q P) . NIL . (NORMAL#3) . NIL . NORMAL . NIL . 3 .)(|∀P Q R.(P∨Q⊃R)≡(P⊃R)∧(Q⊃R)| . (AXIOM (TM& . |∀P Q R.(P∨Q⊃R)≡(P⊃R)∧(Q⊃R)|)) . (R Q P) . NIL . (NORMAL#4) . NIL . NORMAL . NIL . 4 .)(|∀P Q.¬(P∨Q)≡¬P∧¬Q| . (AXIOM (TM& . |∀P Q.¬(P∨Q)≡¬P∧¬Q|)) . (R Q P) . NIL . (NORMAL#5) . NIL . NORMAL . NIL . 5 .)(|∀P Q.¬(P∧Q)≡¬P∨¬Q| . (AXIOM (TM& . |∀P Q.¬(P∧Q)≡¬P∨¬Q|)) . (R Q P) . NIL . (NORMAL#6) . NIL . NORMAL . NIL . 6 .)(|∀P Q.P≡(Q⊃P)∧(¬Q⊃P)| . (AXIOM (TM& . |∀P Q.P≡(Q⊃P)∧(¬Q⊃P)|)) . (R Q P) . NIL . (NORMAL#7) . NIL . NORMAL . NIL . 7 .)(|∀P Q R.(Q⊃R)∧(IF P THEN Q ELSE R)⊃R| . (DERIVE (TM& . |∀P Q R.(Q⊃R)∧(IF P THEN Q ELSE R)⊃R|) ((LR&)) NIL) . (R Q P) . NIL . NIL . NIL . NORMAL . NIL . 8 .)(|∀N.¬N<N| . (AXIOM (TM& . |∀N.¬N<N|)) . (LESSP M N K J I) . NIL . (NATNUM#7) . NIL . NATNUM . NIL . 7 .)(|∀N M K.N<M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M<K⊃N<K|)) . (LESSP M N K J I) . NIL . (NATNUM#8) . NIL . NATNUM . NIL . 8 .)(|∀N.¬N<0| . (AXIOM (TM& . |∀N.¬N<0|)) . (LESSP M N K J I) . NIL . (NATNUM#9) . NIL . NATNUM . NIL . 9 .)(|∀N.NATNUM(N')| . (AXIOM (TM& . |∀N.NATNUM(N')|)) . (ADD1 M N K J I) . NIL . (NATNUM#10) . NIL . NATNUM . NIL . 10 .)(|∀N.N<N'| . (AXIOM (TM& . |∀N.N<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#11) . NIL . NATNUM . NIL . 11 .)(|∀N M.¬N<M⊃M<N'| . (AXIOM (TM& . |∀N M.¬N<M⊃M<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#12) . NIL . NATNUM . NIL . 12 .)(|∀N M.N'<M'≡N<M| . (AXIOM (TM& . |∀N M.N'<M'≡N<M|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#13) . NIL . NATNUM . NIL . 13 .)(|∀N M.N'=M'≡N=M| . (AXIOM (TM& . |∀N M.N'=M'≡N=M|)) . (ADD1 M N K J I) . NIL . (NATNUM#14) . NIL . NATNUM . NIL . 14 .)(|∀N.¬N=0⊃0<N| . (AXIOM (TM& . |∀N.¬N=0⊃0<N|)) . (LESSP M N K J I) . NIL . (NATNUM#15) . NIL . NATNUM . NIL . 15 .)(|∀N.0<N'| . (AXIOM (TM& . |∀N.0<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#16) . NIL . NATNUM . NIL . 16 .)(|∀N.¬N'=0| . (AXIOM (TM& . |∀N.¬N'=0|)) . (ADD1 M N K J I) . NIL . (NATNUM#17) . NIL . NATNUM . NIL . 17 .)(NIL . (DECL PRED (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT)) . ((PRED . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#18 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 18 .)(|∀N.PRED(N')=N| . (DEFAX PRED (TM& . |∀N.PRED(N')=N|)) . ((PRED . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#19 . NIL . DEFINED .)) ADD1 M N K J I) . NIL . (NATNUM#19) . NIL . NATNUM . NIL . 19 .)(|∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))| . (AXIOM (TM& . |∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))|)) . (ADD1 M N K J I SET C B A) . NIL . (INDUCTION#1) . NIL . INDUCTION . NIL . 1 .)(NIL . (DECL NPARS (TYPE: (TY& . GROUND*))) . ((NPARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 2 .)(NIL . (DECL NDF (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((NDF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#3 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 3 .)(NIL . (DECL ZCASE (TYPE: (TY& . |(GROUND*)→GROUND|))) . ((ZCASE . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#4 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 4 .)(|∀N.¬N=N'| . (AXIOM (TM& . |∀N.¬N=N'|)) . (ADD1 M N K J I) . NIL . (LESSEQ#1) . NIL . LESSEQ . NIL . 1 .)(NIL . (DECL LESSEQ (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (INFIXNAME: ≤) (BINDINGPOWER: 920)) . ((LESSEQ . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . LESSEQ#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . LESSEQ . NIL . 2 .)(NIL . (DECL EPSILON (TYPE: (TY& . |(GROUND⊗(@AV))→TRUTHVAL|)) (INFIXNAME: ε) (BINDINGPOWER: 925)) . ((EPSILON . (|(GROUND⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#3 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 3 .)(|∀AV XV.XVεAV≡AV(XV)| . (DEFINE EPSILON (TM& . |∀AV XV.XVεAV≡AV(XV)|) NIL) . ((EPSILON . (|(GROUND⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#4 . NIL . DEFINED .)) URELEMENT ZV YV XV BV AV) . NIL . (SETS#4) . NIL . SETS . NIL . 4 .)(NIL . (DECL ALL (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((ALL . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#1 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . SUMS . NIL . 1 .)(NIL . (DECL SOME (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((SOME . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#2 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . SUMS . NIL . 2 .)(NIL . (DECL (NUMSEQ F) (TYPE: (TY& . GROUND→GROUND))) . ((F . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#3 . NIL . VARIABLE .)) (NUMSEQ . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#3 . NIL . VARIABLE .))) . NIL . NIL . NIL . SUMS . NIL . 3 .)(|∀N.NATNUM(PRED(N))| . (AXIOM (TM& . |∀N.NATNUM(PRED(N))|)) . (ADD1 M N K J I PRED) . NIL . (NATNUM#20) . NIL . NATNUM . NIL . 20 .)(|∀N K.0+N=N∧K'+N=(K+N)'| . (DEFAX PLUS (TM& . |∀N K.0+N=N∧K'+N=(K+N)'|)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#21 . NIL . DEFINED .)) ADD1 M N K J I) . NIL . (NATNUM#21) . NIL . NATNUM . NIL . 21 .)(|∀NDF ZCASE NDEF.(∃FUN.(∀NPARS N.FUN(0,NPARS)=ZCASE(NPARS)∧ FUN(N',NPARS)= NDEF(N,FUN(N,NDF(N,NPARS)),NPARS)))| . (AXIOM (TM& . |∀NDF ZCASE NDEF.(∃FUN.(∀NPARS N.FUN(0,NPARS)=ZCASE(NPARS)∧ FUN(N',NPARS)= NDEF(N,FUN(N,NDF(N,NPARS)),NPARS)))|)) . (ADD1 M N K J I NPARS NDF ZCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#5 . NIL . VARIABLE .)) (NDEF . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#5 . NIL . VARIABLE .))) . NIL . (INDUCTION#5) . NIL . INDUCTION . NIL . 5 .)(|∀A2.(∀N M.A2(0,N)∧A2(N,0)∧(A2(N,M)⊃A2(N',M')))⊃(∀N M.A2(N,M))| . (AXIOM (TM& . |∀A2.(∀N M.A2(0,N)∧A2(N,0)∧(A2(N,M)⊃A2(N',M')))⊃(∀N M.A2(N,M))|)) . (ADD1 M N K J I (A2 . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#6 . NIL . VARIABLE .))) . NIL . (INDUCTION#6) . NIL . INDUCTION . NIL . 6 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 7 .)(|∀AV BV.(∀XV.XVεAV≡XVεBV)⊃AV=BV| . (AXIOM (TM& . |∀AV BV.(∀XV.XVεAV≡XVεBV)⊃AV=BV|)) . (URELEMENT ZV YV XV BV AV EPSILON) . NIL . (SETS#5) . NIL . SETS . NIL . 5 .)(NIL . (DECL INTERSECTION (TYPE: (TY& . |((@AV)⊗(@AV))→(@AV)|)) (INFIXNAME: ∩) (BINDINGPOWER: 950) (PREFIXNAME: INTERSECTION)) . ((INTERSECTION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INTERSECTION) (BINDP& . 950) (INFIX& . ∩)) . SETS#6 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 6 .)(|∀AV BV.AV∩BV=(λXV.AV(XV)∧BV(XV))| . (DEFINE INTERSECTION (TM& . |∀AV BV.AV∩BV=(λXV.AV(XV)∧BV(XV))|) NIL) . ((INTERSECTION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INTERSECTION) (BINDP& . 950) (INFIX& . ∩)) . SETS#7 . NIL . DEFINED .)) URELEMENT ZV YV XV BV AV) . NIL . (SETS#7) . NIL . SETS . NIL . 7 .)(NIL . (DECL UNION (TYPE: (TY& . |((@AV)⊗(@AV))→(@AV)|)) (INFIXNAME: ∪) (BINDINGPOWER: 950) (PREFIXNAME: UNION)) . ((UNION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . UNION) (BINDP& . 950) (INFIX& . ∪)) . SETS#8 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 8 .)(|∀AV BV.AV∪BV=(λXV.AV(XV)∨BV(XV))| . (DEFINE UNION (TM& . |∀AV BV.AV∪BV=(λXV.AV(XV)∨BV(XV))|) NIL) . ((UNION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . UNION) (BINDP& . 950) (INFIX& . ∪)) . SETS#9 . NIL . DEFINED .)) URELEMENT ZV YV XV BV AV) . NIL . (SETS#9) . NIL . SETS . NIL . 9 .)(NIL . (DECL INCLUSION (TYPE: (TY& . |((@AV)⊗(@AV))→TRUTHVAL|)) (INFIXNAME: ⊂) (BINDINGPOWER: 920) (PREFIXNAME: INCLUSION)) . ((INCLUSION . (|((@AV)⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INCLUSION) (BINDP& . 920) (INFIX& . ⊂)) . SETS#10 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 10 .)(|∀AV BV.AV⊂BV≡(∀XV.AV(XV)⊃BV(XV))| . (DEFINE INCLUSION (TM& . |∀AV BV.AV⊂BV≡(∀XV.AV(XV)⊃BV(XV))|) NIL) . ((INCLUSION . (|((@AV)⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INCLUSION) (BINDP& . 920) (INFIX& . ⊂)) . SETS#11 . NIL . DEFINED .)) URELEMENT ZV YV XV BV AV) . NIL . (SETS#11) . NIL . SETS . NIL . 11 .)(|EMPTYSET=(λXV.FALSE)| . (DEFAX EMPTYSET (TM& . |EMPTYSET=(λXV.FALSE)|)) . ((EMPTYSET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#12 . NIL . DEFINED .)) URELEMENT ZV YV XV) . NIL . (SETS#12) . NIL . SETS . NIL . 12 .)(|∀AV.EMPTYP(AV)=(∀XV.¬AV(XV))| . (DEFAX EMPTYP (TM& . |∀AV.EMPTYP(AV)=(∀XV.¬AV(XV))|)) . ((EMPTYP . (|(GROUND→TRUTHVAL)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#13 . NIL . DEFINED .)) URELEMENT ZV YV XV BV AV) . NIL . (SETS#13) . NIL . SETS . NIL . 13 .)(|∀N.URELEMENT(N)| . (AXIOM (TM& . |∀N.URELEMENT(N)|)) . (M N K J I ZV YV XV URELEMENT) . NIL . (SETS#14) . NIL . SETS . NIL . 14 .)(NIL . (DECL SUM (TYPE: (TY& . |((@NUMSEQ)⊗(@N))→(@N)|)) (SYNTYPE: CONSTANT)) . ((SUM . (|((@NUMSEQ)⊗(@N))→(@N)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#4 . NIL . CONSTANT .)) N NUMSEQ) . NIL . NIL . NIL . SUMS . NIL . 4 .)(NIL . (DECL SETSEQ (TYPE: (TY& . |(@N)→(@SET)|))) . ((SETSEQ . (|(@N)→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#5 . NIL . VARIABLE .)) SET N) . NIL . NIL . NIL . SUMS . NIL . 5 .)(|∀N M.NATNUM(N+M)| . (AXIOM (TM& . |∀N M.NATNUM(N+M)|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#22) . NIL . NATNUM . NIL . 22 .)(|∀N.N+0=N| . (AXIOM (TM& . |∀N.N+0=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#23) . NIL . NATNUM . NIL . 23 .)(|∀N.1+N=N'∧N+1=N'| . (AXIOM (TM& . |∀N.1+N=N'∧N+1=N'|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#24) . NIL . NATNUM . NIL . 24 .)(|∀N K.N+K'=(N+K)'| . (AXIOM (TM& . |∀N K.N+K'=(N+K)'|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#25) . NIL . NATNUM . NIL . 25 .)(|∀N K M.K+M=K+N≡M=N| . (AXIOM (TM& . |∀N K M.K+M=K+N≡M=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#26) . NIL . NATNUM . NIL . 26 .)(|∀N K M.M+K=N+K≡M=N| . (AXIOM (TM& . |∀N K M.M+K=N+K≡M=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#27) . NIL . NATNUM . NIL . 27 .)(|∀N K.N+K=0≡N=0∧K=0| . (AXIOM (TM& . |∀N K.N+K=0≡N=0∧K=0|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#28) . NIL . NATNUM . NIL . 28 .)(|∀K N.K+N=N+K| . (AXIOM (TM& . |∀K N.K+N=N+K|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#29) . NIL . NATNUM . NIL . 29 .)(|∀N K.0*N=0∧N'*K=N*K+K| . (DEFAX TIMES (TM& . |∀N K.0*N=0∧N'*K=N*K+K|)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . NATNUM#30 . NIL . DEFINED .)) ADD1 PLUS M N K J I) . NIL . (NATNUM#30) . NIL . NATNUM . NIL . 30 .)(NIL . (DECL INDFN (TYPE: (TY& . |(GROUND⊗(@ARB))→(@ARB)|))) . ((INDFN . (|(GROUND⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#8 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . INDUCTION . NIL . 8 .)(NIL . (DECL (DEF_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((DEF_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#9 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . INDUCTION . NIL . 9 .)(|∀AV BV.AV⊂BV∧BV⊂AV⊃AV=BV| . (AXIOM (TM& . |∀AV BV.AV⊂BV∧BV⊂AV⊃AV=BV|)) . (URELEMENT ZV YV XV BV AV INCLUSION) . NIL . (SETFACTS#1) . NIL . SETFACTS . NIL . 1 .)(NIL . (DECL UN (TYPE: (TY& . |((@SETSEQ)⊗(@N))→(@SET)|)) (SYNTYPE: CONSTANT)) . ((UN . (|((@SETSEQ)⊗(@N))→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#6 . NIL . CONSTANT .)) SET N SETSEQ) . NIL . NIL . NIL . SUMS . NIL . 6 .)(|∀N A.ALL(0,A)∧(ALL(N',A)≡A(N)∧ALL(N,A))| . (DEFAX ALL (TM& . |∀N A.ALL(0,A)∧(ALL(N',A)≡A(N)∧ALL(N,A))|)) . (ADD1 M N K J I SET C B A (ALL . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#7 . NIL . DEFINED .))) . NIL . (SUMS#7) . NIL . SUMS . NIL . 7 .)(|∀N A.¬SOME(0,A)∧(SOME(N',A)≡A(N)∨SOME(N,A))| . (DEFAX SOME (TM& . |∀N A.¬SOME(0,A)∧(SOME(N',A)≡A(N)∨SOME(N,A))|)) . (ADD1 M N K J I SET C B A (SOME . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#8 . NIL . DEFINED .))) . NIL . (SUMS#8) . NIL . SUMS . NIL . 8 .)(|∀N NUMSEQ.SUM(NUMSEQ,0)=0∧SUM(NUMSEQ,N')=SUM(NUMSEQ,N)+NUMSEQ(N)| . (DEFAX SUM (TM& . |∀N NUMSEQ.SUM(NUMSEQ,0)=0∧SUM(NUMSEQ,N')=SUM(NUMSEQ,N)+NUMSEQ(N)|)) . (ADD1 PLUS M N K J I F NUMSEQ (SUM . (|((@NUMSEQ)⊗(@N))→(@N)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#9 . NIL . DEFINED .))) . NIL . (SUMS#9) . NIL . SUMS . NIL . 9 .)(|∀N SETSEQ.UN(SETSEQ,0)=EMPTYSET∧UN(SETSEQ,N')=UN(SETSEQ,N)∪SETSEQ(N)| . (DEFAX UN (TM& . |∀N SETSEQ.UN(SETSEQ,0)=EMPTYSET∧UN(SETSEQ,N')=UN(SETSEQ,N)∪SETSEQ(N)|)) . (ADD1 M N K J I SET ZV YV XV URELEMENT BV AV UNION EMPTYSET SETSEQ (UN . (|((@SETSEQ)⊗(@N))→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#10 . NIL . DEFINED .))) . NIL . (SUMS#10) . NIL . SUMS . NIL . 10 .)(NIL . (DECL DISJ_PAIR (TYPE: (TY& . |((@SET)⊗(@SET))→TRUTHVAL|))) . ((DISJ_PAIR . (|((@SET)⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#11 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . SUMS . NIL . 11 .)(|∀N M.NATNUM(M*N)| . (AXIOM (TM& . |∀N M.NATNUM(M*N)|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#31) . NIL . NATNUM . NIL . 31 .)(|∀N.N*0=0∧1*N=N∧N*1=N| . (AXIOM (TM& . |∀N.N*0=0∧1*N=N∧N*1=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#32) . NIL . NATNUM . NIL . 32 .)(|∀N K.N*K'=N*K+N| . (AXIOM (TM& . |∀N K.N*K'=N*K+N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#33) . NIL . NATNUM . NIL . 33 .)(|∀N K M.¬K=0⊃K*M=K*N≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃K*M=K*N≡M=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#34) . NIL . NATNUM . NIL . 34 .)(|∀N K M.¬K=0⊃M*K=N*K≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃M*K=N*K≡M=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#35) . NIL . NATNUM . NIL . 35 .)(|∀N M.N*M=M*N| . (AXIOM (TM& . |∀N M.N*M=M*N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#36) . NIL . NATNUM . NIL . 36 .)(|∀N K.¬N=0⊃N*K=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃N*K=0≡K=0|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#37) . NIL . NATNUM . NIL . 37 .)(|∀N K.¬N=0⊃K*N=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃K*N=0≡K=0|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#38) . NIL . NATNUM . NIL . 38 .)(|∀N K M.N*(K+M)=N*K+N*M| . (AXIOM (TM& . |∀N K M.N*(K+M)=N*K+N*M|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#39) . NIL . NATNUM . NIL . 39 .)(|∀N M K.(M+K)*N=M*N+K*N| . (AXIOM (TM& . |∀N M K.(M+K)*N=M*N+K*N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#40) . NIL . NATNUM . NIL . 40 .)(|∀INDFN ARB.(∃DEF_FUN.(∀N.DEF_FUN(0)=ARB∧DEF_FUN(N')=INDFN(N,DEF_FUN(N))))| . (AXIOM (TM& . |∀INDFN ARB.(∃DEF_FUN.(∀N.DEF_FUN(0)=ARB∧DEF_FUN(N')=INDFN(N,DEF_FUN(N))))|)) . (ADD1 M N K J I ARB2 ARB1 ARB INDFN DEF_FUN) . NIL . (INDUCTION#10) . NIL . INDUCTION . NIL . 10 .)(|¬(∃DESC.(∀N.DESC(N')<DESC(N)))| . (AXIOM (TM& . |¬(∃DESC.(∀N.DESC(N')<DESC(N)))|)) . (LESSP ADD1 M N K J I (DESC . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#11 . NIL . VARIABLE .))) . NIL . (INDUCTION#11) . NIL . INDUCTION . NIL . 11 .)(|∀A N.(∀M.M<N⊃A(M))≡ALL(N,A)| . (AXIOM (TM& . |∀A N.(∀M.M<N⊃A(M))≡ALL(N,A)|)) . (LESSP ADD1 M N K J I SET C B A ALL) . NIL . (SUMFACTS#1) . NIL . SUMFACTS . NIL . 1 .)(|∀A N.(∃M.M<N∧A(M))≡SOME(N,A)| . (AXIOM (TM& . |∀A N.(∃M.M<N∧A(M))≡SOME(N,A)|)) . (LESSP ADD1 M N K J I SET C B A SOME) . NIL . (SUMFACTS#2) . NIL . SUMFACTS . NIL . 2 .)(|∀SETSEQ N M.M<N⊃SETSEQ(M)⊂UN(SETSEQ,N)| . (AXIOM (TM& . |∀SETSEQ N M.M<N⊃SETSEQ(M)⊂UN(SETSEQ,N)|)) . (LESSP ADD1 M N K J I SET ZV YV XV URELEMENT BV AV UNION INCLUSION EMPTYSET SETSEQ UN) . NIL . (SUMFACTS#3) . NIL . SUMFACTS . NIL . 3 .)(|∀NUMSEQ N.(∀M.M<N⊃NATNUM(NUMSEQ(M)))⊃NATNUM(SUM(NUMSEQ,N))| . (AXIOM (TM& . |∀NUMSEQ N.(∀M.M<N⊃NATNUM(NUMSEQ(M)))⊃NATNUM(SUM(NUMSEQ,N))|)) . (LESSP ADD1 M N K J I F NUMSEQ SUM) . NIL . (SUMFACTS#4) . NIL . SUMFACTS . NIL . 4 .)(|∀M N.M≤N=(M=N∨M<N)| . (DEFINE LESSEQ (TM& . |∀M N.M≤N=(M=N∨M<N)|) NIL) . ((LESSEQ . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . LESSEQ#3 . NIL . DEFINED .)) LESSP M N K J I) . NIL . (LESSEQ#3 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1) . NIL . LESSEQ . NIL . 3 .)(|∀N M.N'≤M'≡N≤M| . (AXIOM (TM& . |∀N M.N'≤M'≡N≤M|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#4) . NIL . LESSEQ . NIL . 4 .)(|∀N M K.N≤M∧M≤K⊃N≤K| . (AXIOM (TM& . |∀N M K.N≤M∧M≤K⊃N≤K|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#5) . NIL . LESSEQ . NIL . 5 .)(|∀N M K.N<M∧M≤K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M≤K⊃N<K|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#6) . NIL . LESSEQ . NIL . 6 .)(|∀N.0≤N| . (AXIOM (TM& . |∀N.0≤N|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#7) . NIL . LESSEQ . NIL . 7 .)(|∀N.1≤N'| . (AXIOM (TM& . |∀N.1≤N'|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#8) . NIL . LESSEQ . NIL . 8 .)(|∀N M.N'<M⊃¬M=0| . (AXIOM (TM& . |∀N M.N'<M⊃¬M=0|)) . (LESSP ADD1 M N K J I) . NIL . (LESSEQ#9) . NIL . LESSEQ . NIL . 9 .)(|∀M N.M'<N⊃M<N| . (AXIOM (TM& . |∀M N.M'<N⊃M<N|)) . (LESSP ADD1 M N K J I) . NIL . (LESSEQ#10) . NIL . LESSEQ . NIL . 10 .)(|∀M N.M'≤N⊃M≤N| . (AXIOM (TM& . |∀M N.M'≤N⊃M≤N|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#11) . NIL . LESSEQ . NIL . 11 .)(|∀N M.N≤M⊃N≤M'| . (AXIOM (TM& . |∀N M.N≤M⊃N≤M'|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#12) . NIL . LESSEQ . NIL . 12 .)(|∀N M.M<N'≡M≤N| . (AXIOM (TM& . |∀N M.M<N'≡M≤N|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#13) . NIL . LESSEQ . NIL . 13 .)(|∀M N.M<N=M'≤N| . (AXIOM (TM& . |∀M N.M<N=M'≤N|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#14) . NIL . LESSEQ . NIL . 14 .)(|∀N M.N≤M∧M≤N⊃N=M| . (AXIOM (TM& . |∀N M.N≤M∧M≤N⊃N=M|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#15) . NIL . LESSEQ . NIL . 15 .)(|∀N M.M<N∨M=N∨N<M| . (AXIOM (TM& . |∀N M.M<N∨M=N∨N<M|)) . (LESSP M N K J I) . NIL . (LESSEQ#16) . NIL . LESSEQ . NIL . 16 .)(|∀M N.M-0=M∧M-N'=PRED(M-N)| . (DEFINE MINUS (TM& . |∀M N.M-0=M∧M-N'=PRED(M-N)|) (USE (LR& INDUCTION#5))) . ((MINUS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 940) (INFIX& . -)) . MINUS#2 . NIL . DEFINED .)) ADD1 M N K J I PRED) . NIL . (MINUS#2 INDUCTION#5 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9) . NIL . MINUS . NIL . 2 .)(|∀N K.NATNUM(K-N)| . (AXIOM (TM& . |∀N K.NATNUM(K-N)|)) . (ADD1 M N K J I PRED MINUS) . NIL . (MINUS#3) . NIL . MINUS . NIL . 3 .)(|∀N M.N<M⊃0<M-N| . (AXIOM (TM& . |∀N M.N<M⊃0<M-N|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#4) . NIL . MINUS . NIL . 4 .)(|∀N.0<N⊃PRED(N)'=N| . (AXIOM (TM& . |∀N.0<N⊃PRED(N)'=N|)) . (LESSP ADD1 M N K J I PRED) . NIL . (MINUS#5) . NIL . MINUS . NIL . 5 .)(|∀N M.N≤M⊃M'-N=(M-N)'| . (AXIOM (TM& . |∀N M.N≤M⊃M'-N=(M-N)'|)) . (LESSP ADD1 M N K J I PRED LESSEQ MINUS) . NIL . (MINUS#6) . NIL . MINUS . NIL . 6 .)(|∀N M.N<M⊃M-N=(M-N')'| . (AXIOM (TM& . |∀N M.N<M⊃M-N=(M-N')'|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#7) . NIL . MINUS . NIL . 7 .)(|∀N M.M<N⊃N-M'<N| . (AXIOM (TM& . |∀N M.M<N⊃N-M'<N|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#8) . NIL . MINUS . NIL . 8 .)(|∀N.N-N=0| . (AXIOM (TM& . |∀N.N-N=0|)) . (ADD1 M N K J I PRED MINUS) . NIL . (MINUS#9) . NIL . MINUS . NIL . 9 .)(|∀N.0<N⊃N-PRED(N)=1| . (AXIOM (TM& . |∀N.0<N⊃N-PRED(N)=1|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#10) . NIL . MINUS . NIL . 10 .)(|∀N M.M≤N⊃M-N=0| . (AXIOM (TM& . |∀N M.M≤N⊃M-N=0|)) . (LESSP ADD1 M N K J I PRED LESSEQ MINUS) . NIL . (MINUS#11) . NIL . MINUS . NIL . 11 .)(|∀N M K.K<N∧M<N-K≡M+K<N| . (AXIOM (TM& . |∀N M K.K<N∧M<N-K≡M+K<N|)) . (LESSP ADD1 PLUS M N K J I PRED MINUS) . NIL . (MINUS#12) . NIL . MINUS . NIL . 12 .)(|∀N K M.N≤M∧1≤K⊃N'≤M+K| . (AXIOM (TM& . |∀N K M.N≤M∧1≤K⊃N'≤M+K|)) . (LESSP ADD1 PLUS M N K J I LESSEQ) . NIL . (MINUS#13) . NIL . MINUS . NIL . 13 .)(|∀K N M.1≤K∧M+K=N'∧N≤M⊃1=K∧N=M| . (AXIOM (TM& . |∀K N M.1≤K∧M+K=N'∧N≤M⊃1=K∧N=M|)) . (LESSP ADD1 PLUS M N K J I LESSEQ) . NIL . (MINUS#14) . NIL . MINUS . NIL . 14 .)(|∀A B.DISJ_PAIR(A,B)=EMPTYP(A∩B)| . (DEFINE DISJ_PAIR (TM& . |∀A B.DISJ_PAIR(A,B)=EMPTYP(A∩B)|) NIL) . (SET C B A ZV YV XV URELEMENT BV AV INTERSECTION EMPTYP (DISJ_PAIR . (|((@SET)⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#12 . NIL . DEFINED .))) . NIL . (SUMS#12 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 SETS#14) . NIL . SUMS . NIL . 12 .)(NIL . (DECL DISJOINT (TYPE: (TY& . |((GROUND→(@SET))⊗GROUND)→TRUTHVAL|))) . ((DISJOINT . (|((GROUND→(@SET))⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#13 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . SUMS . NIL . 13 .)(|∀N SETSEQ.DISJOINT(SETSEQ,0)∧ DISJOINT(SETSEQ,N')= (DISJOINT(SETSEQ,N)∧DISJ_PAIR(UN(SETSEQ,N),SETSEQ(N)))| . (DEFAX DISJOINT (TM& . |∀N SETSEQ.DISJOINT(SETSEQ,0)∧ DISJOINT(SETSEQ,N')= (DISJOINT(SETSEQ,N)∧DISJ_PAIR(UN(SETSEQ,N),SETSEQ(N)))|)) . (ADD1 M N K J I SET C B A ZV YV XV URELEMENT BV AV INTERSECTION UNION EMPTYSET EMPTYP SETSEQ UN DISJ_PAIR (DISJOINT . (|((GROUND→(@SET))⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#14 . NIL . DEFINED .))) . NIL . (SUMS#14) . NIL . SUMS . NIL . 14 .)